Require Import AutoSep.

Fixpoint sll (ls : list W) (p : W) : HProp :=
  match ls with
    | nil => [| p = 0 |]
    | x :: ls' => [| p <> 0 |] * Ex p', (p ==*> x, p') * sll ls' p'
  end%Sep.

Definition revS := SPEC("x") reserving 3
  Ex ls,
  PRE[V] sll ls (V "x")
  POST[R] sll (rev ls) R.

Definition revM := bmodule "rev" {{
  bfunction "rev"("x", "acc", "tmp1", "tmp2") [revS]
    "acc" <- 0;;
    [Ex ls, Ex accLs,
      PRE[V] sll ls (V "x") * sll accLs (V "acc")
      POST[R] sll (rev_append ls accLs) R ]
    While ("x" <> 0) {
      "tmp2" <- "x";;
      "tmp1" <- "x" + 4;;
      "x" <-* "tmp1";;
      "tmp1" *<- "acc";;
      "acc" <- "tmp2"
    };;
    Return "acc"
  end
}}.


Theorem revMOk : moduleOk revM.
Proof.
  vcgen.
  post.
  post.
  evaluate auto_ext.
  post.
  evaluate auto_ext.
  descend.
  Focus 1.
  step auto_ext.
  step auto_ext.
  Focus 1.
  step auto_ext.
  Focus 1.
  step auto_ext.
  step auto_ext.
  step auto_ext.
  Focus 1.
  descend.
  post.
  evaluate auto_ext.
  Focus 1.
  post.
  evaluate auto_ext.
  descend.
  Focus 1.
  step auto_ext.
  step auto_ext.
Theorem nil_bwd : forall ls (p : W), p = 0
  -> [| ls = nil |] ===> sll ls p.
Proof.
  destruct ls; sepLemma.
Qed.
Definition hints : TacPackage.
  prepare tt nil_bwd.
Defined.
  step hints.
  step hints.
  step hints.
  step hints.
  step hints.
  Hint Rewrite <- rev_alt : sepFormula.
  step hints.
  step hints.
  Focus 1.
  post.
  evaluate hints.
  Focus 1.
  post.
  Theorem cons_fwd : forall ls (p : W), p <> 0
  -> sll ls p ===> Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
  destruct ls; sepLemma.
Qed.
  Definition hints2 : TacPackage.
    prepare cons_fwd nil_bwd.
  Defined.
  evaluate hints2.
  descend.
  Focus 1.
  sep hints2.
Theorem cons_bwd : forall ls (p : W), p <> 0
  -> (Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p') ===> sll ls p.
Proof.
  destruct ls; sepLemma;
    match goal with
      | [ H : _ :: _ = _ :: _ |- _ ] => injection H; sepLemma
    end.
Qed.
  Definition hints3 : TacPackage.
    prepare cons_fwd (nil_bwd, cons_bwd).
  Defined.
  step hints3.
  step hints3.
  step hints3.
  step hints3.
  step hints3.
  step hints3.
  Focus 1.
  post.
  evaluate hints3.
  post.
  evaluate hints3.
  sep hints3.
Theorem nil_fwd : forall ls (p : W), p = 0
  -> sll ls p ===> [| ls = nil |].
Proof.
  destruct ls; sepLemma.
Qed.
  Definition hints4 : TacPackage.
    prepare (nil_fwd, cons_fwd) (nil_bwd, cons_bwd).
  Defined.
  step hints4.
  step hints4.
  step hints4.
Qed.

(*
  vcgen; sep hints.
Qed.

Theorem sll_extensional : forall ls (p : W), HProp_extensional (sll ls p).
Proof.
  destruct ls; reflexivity.
Qed.

Hint Immediate sll_extensional.

Theorem nil_bwd : forall ls (p : W), p = 0
  -> [| ls = nil |] ===> sll ls p.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem nil_fwd : forall ls (p : W), p = 0
  -> sll ls p ===> [| ls = nil |].
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_fwd : forall ls (p : W), p <> 0
  -> sll ls p ===> Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_bwd : forall ls (p : W), p <> 0
  -> (Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p') ===> sll ls p.
Proof.
  destruct ls; sepLemma;
    match goal with
      | [ H : _ :: _ = _ :: _ |- _ ] => injection H; sepLemma
    end.
Qed.

Definition hints : TacPackage.
  prepare (nil_fwd, cons_fwd) (nil_bwd, cons_bwd).
Defined.

Hint Rewrite <- rev_alt : sepFormula.
*)
